Nuprl Lemma : decidable__ex_int_seg
13,42
postcript
pdf
i
,
j
:
,
F
:({
i
..
j
}
{u}). (
k
:{
i
..
j
}. Dec(
F
(
k
)))
Dec(
k
:{
i
..
j
}.
F
(
k
))
latex
Up
int
2
,
int
2
Definitions
t
T
,
x
(
s
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
False
,
A
,
{...
i
}
,
A
B
,
P
&
Q
,
i
j
<
k
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
{
i
..
j
}
,
P
Q
,
Dec(
P
)
,
{
T
}
Lemmas
decidable
wf
,
int
seg
wf
,
decidable
le
,
le
wf
,
int
lower
wf
,
int
lower
ind
,
not
wf
,
decidable
int
equal
origin
i, j:
, F:({i..j
}
{u}). (k:{i..j}. Dec(F(k))) 
Dec(
k:{i..j}. F(k)) i, j:, F:({i..j}{u}). (k:{i..j}. Dec(F(k))) Dec(k:{i..j}. F(k)) 
T Qx:A. B(x)
A
B j < k
x. t(x)x:A. B(x)}
Q